State machines, also referred to as state charts, are tools for designing and organizing the way a device, computer program, or other (such as technical) process works, such that an entity or any of its components is in one of a number of possible states, or in an “and” combination of states, wherein well-defined conditional transitions exist between these states. State machines are useful in describing event-driven behaviors in which the system may take action or change its state in response to events such as user events, system events or others.
A UML state machine or statechart is an object-based variant of a state chart, which is adapted and extended by the Unified Modeling Language (UML) notation. UML state machines attempt to overcome the main limitations of traditional finite-state machines, while retaining their main benefits. UML statecharts introduce new concepts and features over traditional state charts, such as hierarchically nested states, orthogonal regions, extending the notion of actions, and other additions.
UML state machines have characteristics of both Mealy machines and Moore machines. Thus, UML state machines support actions that may depend on the state the system is at, as well as on the triggering event as in Mealy machines, and entry and exit actions associated with states rather than with transitions, as in Moore machines.
Although the specification of UML state machines is not formal, the executable sub-set thereof is well defined to allow tool vendors to support simulation and automatic code generation out of UML diagrams. This brings up the need for many purposes such as verification of UML state machines. In particular, formal verification is important for high integrity and safety critical domains. Formal verification relates to checking whether a condition holds for a system at all states, for example “the system is always in a stable state”. The verification tool either approves that the condition holds at all times, or provides a counterexample.
However, UML statecharts are generally more complex and have more features than code programs. Therefore, code generation is a complex task, and therefore verification is mainly done by executing specific examples. Other known automatic UML verification tools take a UML statechart and translate, or synthesize it to the input language or format of an existing model checker or verification tool. However, such UML verification tools are limited in their ability to analyze UML statecharts and can handle only a simple sub-set of UML state machine features.